<html>
<head><title></title></head>

<body>

<p>This package is responsible for generating verification conditions
from an AST and type information obtained by the package 
{@code freeboogie.tc}.</p>

<p>Phase:</p>

<ul>

<li>make flow graph reducible (rely on Spec#)</li>

<li>desugar loops: get rid of loops (rely on Spec#)</li>

<li>desugar function calls: get rid of calls</li>

<li>desugar pre- and postconditions and modifies?? (
    recursive calls?
    argument in postconditions?)</li>

<li>passivate program: get rid of havoc and assignments and old</li>

<li>strongest postcondition (build query term)
  &mdash; the input is a DAG with ASSERT/ASSUME in nodes, conceptually</li>

</ul>

<p>How to deal with arrays? Perhaps let the prover interface take
care of it.</p>

<p>TODO: The backend also needs to deal with eliminating sharing
in case the formula DAG gets translated into a string. For example,
Z3 would use FLET to introduce some temporaries and Simplify would
use IFF.</p>

</body>
</html>
